(declare-fun b () Real)
(declare-fun KjafX_new () Real)
(declare-fun c () Real)
(declare-fun e () Real)
(declare-fun a () Real)
(declare-fun s () Real)
(declare-fun l () Real)
(declare-fun f () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun ac () Real)
(declare-fun ts2209uscore0 () Real)
(declare-fun g () Real)
(declare-fun A () Real)
(declare-fun m () Real)
(declare-fun h () Real)
(declare-fun V () Real)
(declare-fun i () Real)
(declare-fun o () Real)
(declare-fun j () Real)
(declare-fun n () Real)
(assert (forall ((ts2209uscore0 Real)) (or (<= 0 (/ 74 KjafX_new (/ a ts2209uscore0))) (>= 0 (/ e n)) (and (>= (/ (/ s ts2209uscore0) aa) d) (>= (/ ts2209uscore0 0) 0)))))
(assert (forall ((k Real)) (or (and (or (and (or (>= 0 (/ b s)) (>= (/ 7 b s) i)) (>= 0 j)) (>= (/ 5 c f) V) (= m 2) (>= 0 g) (<= h V)) (<= 0 (/ 0 l))) (>= 0 V))))
(assert (= b (/ s o)))
(assert (= (/ ac A) a (/ ts2209uscore0 A)))
(check-sat)
